\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Inductive} \coqdocvar{ByteExp} : \coqdockw{Type} :=\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{byte\_exp\_num}    : \coqdocvar{Byte}      \ensuremath{\rightarrow} \coqdocvar{ByteExp}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{byte\_exp\_id}     : \coqdocvar{Id}        \ensuremath{\rightarrow} \coqdocvar{ByteExp}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{byte\_exp\_xor}    : \coqdocvar{ByteExp}   \ensuremath{\rightarrow} \coqdocvar{ByteExp}  \ensuremath{\rightarrow} \coqdocvar{ByteExp}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{byte\_exp\_andbb}  : \coqdocvar{ByteExp}   \ensuremath{\rightarrow} \coqdocvar{ByteExp}  \ensuremath{\rightarrow} \coqdocvar{ByteExp}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{byte\_exp\_shiftl} : \coqdocvar{ByteExp}   \ensuremath{\rightarrow} \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{ByteExp}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{byte\_exp\_shiftr} : \coqdocvar{ByteExp}   \ensuremath{\rightarrow} \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{ByteExp}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{byte\_exp\_matrix} : \coqdocvar{MatrixExp} \ensuremath{\rightarrow} \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{ByteExp}\coqdoceol
\coqdocnoindent
.\coqdoceol
\end{coqdoccode}